package gov.nasa.anml;

import java.util.ArrayList;
import gov.nasa.anml.lifted.*;
import gov.nasa.anml.utility.*;

public class PDDL {

	public String name;
	public ArrayList<Type> types = new ArrayList<Type>();
	public ArrayList<TypeRelation> typeRelations = new ArrayList<TypeRelation>();
	public ArrayList<Object> domainObjects = new ArrayList<Object>();
	public ArrayList<Predicate> predicates = new ArrayList<Predicate>();
	public ArrayList<Function> functions = new ArrayList<Function>();
	public ArrayList<Action> actions = new ArrayList<Action>();
	public ArrayList<ComplexAction> complexActions = new ArrayList<ComplexAction>();

	public Problem prob = new Problem();


	// for collapsing scopes during the translation
	public transient StringBuilder buf = new StringBuilder(); 
	// the names of scopes down to this level.
	// scheme can fail if input scope names play tricky games like
	// a="fly_" b="fly_fly" c="fly", then scope chains ac and b have identical representation, but different depth.
	// to get same depth, just invert the trick -- acb and bac to get two identical depth 2 (zero-based) representations.
	// methods around this either requires
	// a) too much analysis
	// b) incomprehensible symbols [c.f. C++ name mangling; gensym()]
	public transient int depth = -1;  // how deep; actions are at level 0 (Domains are at level -1)
	public transient ArrayList<Parameter> context = new ArrayList<Parameter>(); // the parameters of all parent scopes
	// this is needed for local declarations
	// almost certainly also need an ArrayList of PDDL actions, or ANML units, in order to ensure that PDDL plans respect scoping rules
	// e.g., if there are domain constraints, then all actions need to use the domain-executing predicate in order to force
	// the domain constraints to be included.

	public int bufAppend(SimpleString name) {
		int length = buf.length();
		if (length > 0)
			buf.append('_');
		buf.append(name.v,0,name.length);
		return length;
	}

	public String bufToString() {
		return buf.toString();
	}

	public void bufReset(int length) {
		buf.setLength(length);
	}

	public StringBuilder append(StringBuilder buf) {
		buf.append("(define (domain ").append(name)
		.append(")\n(:requirements :typing :durative-actions)\n(:types");
		for (Type t : types) {
			t.append(buf.append("\n\t"));
		}
		buf.append(" - object");
		for (TypeRelation t : typeRelations) {
			t.append(buf.append("\n\t"));
		}
		buf.append("\n)\n(:predicates (true) (alive) ;; initial state needs to have `(alive)' and it and the goal ought to have `(true)'");
		for (Predicate p : predicates) {
			p.append(buf.append("\n\t"));
		}
		buf.append("\n)\n(:functions");
		for (Function f : functions) {
			f.append(buf.append("\n\t"));
		}
		buf.append("\n)\n(:constants");
		for (Object o : domainObjects) {
			o.append(buf.append("\n\t"));
		}
		buf.append("\n)\n");
		for (Action a : actions) {
			a.append(buf.append('\n'));
		}
		buf.append('\n');
		for (ComplexAction a : complexActions) {
			a.append(buf.append('\n'));
		}
		buf.append("\n\n)\n");
		return buf;
	}


	
	
	public Effect makeEffect(Time time, PDDL.FunctionReference r, PDDL.FloatExpression e) {
		return wrap(time,makeEffect(r,e));
	}
	
	public FloatEffect makeEffect(FunctionReference r, FloatExpression e) {
		return this.new AtomicFloatEffect(Op.assign,r,e);
	}

	public Effect makeEffect(Time time, Op o, PDDL.FunctionReference r, PDDL.FloatExpression e) {
		return wrap(time,makeEffect(o,r,e));
	}
	
	public FloatEffect makeEffect(Op o, PDDL.FunctionReference r, PDDL.FloatExpression e) {
		return this.new AtomicFloatEffect(o,r,e);
	}
	
	public Effect makeEffect(Time time, PDDL.PredicateReference r, PDDL.BooleanExpression expression) {
		return wrap(time,makeEffect(r,expression));
	}
	
	public Effect makeEffect(PDDL.PredicateReference r, PDDL.BooleanExpression expression) {
		if (expression == TrueRef)
			return makeEffect(r,true);
		if (expression == FalseRef)
			return makeEffect(r,false);
		BooleanEffect effT = this.new AtomicBooleanEffect(r,true);
		ConditionalEffect ceffT = this.new ConditionalEffect(expression,effT);
		BooleanEffect effF = this.new AtomicBooleanEffect(r,false);
		UnaryBooleanExpression expressionF = this.new UnaryBooleanExpression(Op.not,expression);
		ConditionalEffect ceffF = this.new ConditionalEffect(expressionF,effF);
		return this.new BinaryEffect(Op.and,ceffT,ceffF);
	}
	
	public Effect makeEffect(BooleanExpression guard, PDDL.PredicateReference r, PDDL.BooleanExpression expression) {
		if (guard == FalseRef)
			return makeEffect(TrueRef,true);
		Effect eff = makeEffect(r,expression);
		return this.new ConditionalEffect(guard,eff);
	}
	
	public Effect makeEffect(BooleanExpression guard, PDDL.PredicateReference r, boolean v) {
		if (guard == FalseRef)
			return makeEffect(TrueRef,true);
		Effect eff = makeEffect(r,v);
		return this.new ConditionalEffect(guard,eff);
	}

	public TimedBooleanEffect makeEffect(Time time,PDDL.PredicateReference r, boolean v) {
		return wrap(time,makeEffect(r,v));
	}
	
	public BooleanEffect makeEffect(PDDL.PredicateReference r, boolean v) {
		return this.new AtomicBooleanEffect(r,v);
	}

	public BooleanExpression negate(BooleanExpression l) {
		if (l instanceof TimedBooleanExpression) {
			TimedBooleanExpression t = (TimedBooleanExpression) l;
			return wrap(t.time,negate(t.e));
		} 
		if (l==FalseRef)
			return TrueRef;
		if (l==TrueRef)
			return FalseRef;
		return wrap(Op.not,l);
	}
	
	public BooleanEffect negate(BooleanEffect l) {
		if (l instanceof TimedBooleanEffect) {
			TimedBooleanEffect t = (TimedBooleanEffect) l;
			return wrap(t.time,negate(t.e));
		} else if (l instanceof AtomicBooleanEffect) {
			AtomicBooleanEffect a = (AtomicBooleanEffect) l;
			return this.new AtomicBooleanEffect(a.ref,!a.v);
		}
		System.err.println("Warning: Don't know how to negate complex effects (killing container with `true' := false).");
		return this.new AtomicBooleanEffect(TrueRef,false);
	}
	
	public BooleanExpression wrap(Op o,BooleanExpression l) {
		return this.new UnaryBooleanExpression(o,l);
	}
	
	public FloatExpression wrap(Op o,FloatExpression l) {
		return this.new UnaryFloatExpression(o,l);
	}

	public Expression wrap(Op o,Expression l) {
		return this.new UnaryExpression(o,l);
	}
	
	public BooleanExpression wrap(Op o,BooleanExpression l, BooleanExpression r) {
		return this.new BinaryBooleanExpression(o,l,r);
	}
	
	public FloatExpression wrap(Op o,FloatExpression l, FloatExpression r) {
		return this.new BinaryFloatExpression(o,l,r);
	}
	
	public BinaryExpression wrap(Op o, Expression l,Expression r) {
		return new BinaryExpression(o,l,r);
	}
	
	public BooleanExpression wrap(Op o,ArrayList<BooleanExpression> operands) {
		return this.new CompoundBooleanExpression(o,operands);
	}
	
	public Effect wrap(Op o,ArrayList<Effect> operands) {
		return this.new CompoundEffect(o,operands);
	}
	
	public BooleanExpression wrap(Time time, BooleanExpression l) {
		if (l.isTimed())
			return l;
		return this.new TimedBooleanExpression(time,l);
	}
	
	public FloatExpression wrap(Time time, FloatExpression l) {
		if (l.isTimed())
			return l;
		return this.new TimedFloatExpression(time,l);
	}
	
	public TimedBooleanEffect wrap(Time time, BooleanEffect e) {
		return this.new TimedBooleanEffect(time,e);
	}
	public TimedFloatEffect wrap(Time time, FloatEffect e) {
		return this.new TimedFloatEffect(time,e);
	}
	
	public <T extends Effect> TimedEffect<T> wrap(Time time, T e) {
		return this.new TimedEffect<T>(time,e);
	}
	

	public BooleanExpression makeTest(PDDL.FloatExpression l, PDDL.FloatExpression r) {
		return this.new RelOp(PDDL.Op.equals,l,r);
	}
	public BooleanExpression makeTest(Op o, PDDL.FloatExpression l, PDDL.FloatExpression r) {
		return this.new RelOp(o,l,r);
	}

	public BooleanExpression makeTest(BooleanExpression l, boolean v) {
		PDDL.BooleanExpression c;
		if (v)
			c = l;
		else
			c = negate(l);
		return c;
	}
	public BooleanExpression makeTest(Op o,BooleanExpression l, boolean v) {
		PDDL.BooleanExpression lt,lf,c;
		switch(o) {
		case lt:
			lf = negate(l);
			if (!v)
				c = wrap(Op.and,lf,FalseRef); // not simplified to assist debugging of models
			else
				c = lf;
			break;
		case gt:
			lt = l;
			if (v)
				c = wrap(Op.and,FalseRef,lt); // not simplified to assist debugging of models
			else
				c = lt;
			break;
		case gte:
			lt = l;
			if(v) 
				c = lt;
			else
				// could omit entirely, but leaving it in helps at least a little in debugging
				c = TrueRef; // perhaps a bug, but not one that would typically destroy solvability (unless nested underneath a not), so simplify
			break;
		case lte:
		case implies:
			lf = negate(l);
			if (v) 
				// could omit entirely, but leaving it in helps at least a little in debugging
				c = TrueRef; // perhaps a bug, but not one that would typically destroy solvability (unless nested underneath a not), so simplify
			else
				c = lf;
			break;
		case equals:
			lt = l;
			lf = negate(l);
			if (v) 
				c = lt;
			else
				c = lf;
			break;
		case and:
			if (v)
				c = l;
			else
				c = FalseRef;
			break;
		case or:
			if (v)
				c = TrueRef;
			else
				c = l;
			break;
		default:
			System.err.println("Operation '" + o + "' not supported, and unexpected, for generic boolean expressions at this time (perhaps never).");
			System.err.println(l);
			c = TrueRef;
		}
		return c;
	}
	
	public PDDL.BooleanExpression makeTest(Op o, BooleanExpression l, BooleanExpression r) {
		if (r == TrueRef) 
			return makeTest(o,l,true);
		if (r == FalseRef) 
			return makeTest(o,l,false);
		
		BooleanExpression lt,lf,rt,rf,c;
		switch(o) {
		case lt:
			lf = negate(l);
			rt = r;
			c = wrap(Op.and,lf,rt);
			break;
		case gt:
			rf = negate(r);
			lt = l;
			c = wrap(Op.and,rf,lt);
			break;
		case gte:
			rf = negate(r);
			lt = l;
			if (lt == FalseRef)
				c = rf;
			else if (lt == TrueRef)
				c = TrueRef;
			else
				c = wrap(Op.or,rf,lt);
			break;
		case lte:
		case implies:
			lf = negate(l);
			rt = r;
			if (lf == FalseRef)
				c = rt;
			else if (lf == TrueRef)
				c = TrueRef;
			else
				c = wrap(Op.or,lf,rt);
			break;
		case equals:
			if (l == TrueRef || l == FalseRef)
				return makeTest(r,l);
			lt = l;
			lf = negate(l);
			rt = r;
			rf = negate(r);
			c = wrap(Op.or,wrap(Op.and, lf, rf), wrap(Op.and, lt,rt));
			//c = doOp(Op.and,doOp(Op.or,negate(l),r),doOp(Op.or,negate(r),l))); 
			// equivalent construction
			//c = doOp(Op.and,doOp(Op.imply,l,r),doOp(Op.imply,r,l))); 
			// but allows this;
			// which has nice parallels with Op.when.
			break;
		case and:
			c = wrap(o,l,r);
			break;
		case or:
			if (l == FalseRef)
				c = r;
			else if (l == TrueRef)
				c = TrueRef;
			else
				c = wrap(o,l,r);
			break;
		default:
			System.err.println("Operation " + o + " not supported, and unexpected, for generic boolean expressions at this time (perhaps never).");
			c = TrueRef;
		}
		return c;
	}
	
	public BooleanExpression makeTest(BooleanExpression l, BooleanExpression r) {
		if (r == TrueRef) 
			return makeTest(l,true);
		if (r == FalseRef) 
			return makeTest(l,false);
		if (l == TrueRef)
			return makeTest(r,true);
		if (l == FalseRef)
			return makeTest(r,false);
		BooleanExpression lt,lf,rt,rf,c;
		lt = l;
		lf = negate(l);
		rt = r;
		rf = negate(r);
		c = wrap(Op.or,wrap(Op.and, lf, rf), wrap(Op.and, lt,rt));
		return c;
	}




	interface Append {
		StringBuilder append(StringBuilder buf);
	}

	class Compound<T extends Append> implements Append {
		public Op o;
		public ArrayList<T> arguments;
		public StringBuilder append(StringBuilder buf) { 
			if (arguments.size() > 1)
				indent(buf);
			buf.append('(').append(o.name);
			for (T arg : arguments) {
				arg.append(buf.append(' '));
			}
			buf.append(')');
			if (arguments.size() > 1)
				dedent(buf);
			return buf;
		}

		public Compound(Op o) {
			this.o = o;
			this.arguments = new ArrayList<T>();
		}
		public Compound(Op o,T a) {
			this.o = o;
			this.arguments = new ArrayList<T>();
			this.arguments.add(a);
			System.err.println("There are better options.");
		}
		public Compound(Op o,T a, T b) {
			this.o = o;
			this.arguments = new ArrayList<T>();
			this.arguments.add(a);
			this.arguments.add(b);
			System.err.println("There are better options.");
		}
		public Compound(Op o, ArrayList<T> args) {
			this.o = o;
			this.arguments = args;
		}
	}

	public interface Expression extends Append {}
	public interface BooleanExpression extends Expression, Append {

		boolean isTimed();	}
	public interface FloatExpression extends Expression, Append {

		boolean isTimed();}
	public interface Effect extends Append {}
	public interface BooleanEffect extends Effect, Append {	}
	public interface FloatEffect extends Effect, Append {}
	public interface Argument extends Append {} 
	public interface Timed<T> extends Append {}






	public class TypeRelation {
		public Type subType;
		public Type superType;

		public TypeRelation(Type subType, Type superType) {
			super();
			this.subType = subType;
			this.superType = superType;
		}

		public StringBuilder append(StringBuilder buf) {
			buf.append(subType.name).append(" - ").append(superType.name);
			return buf;
		}

	}

	public class Type {
		public String name;
		public StringBuilder append(StringBuilder buf) {
			buf.append(name);
			return buf;
		}
		public Type(String name) {
			this.name = name;
		}
	}

	// action lock(Array a) {
	//    duration := 1;
	//    a.lock == false :-> true;
	// }
	// action unlock(Array a) {
	//		duration := 1;
	//		a.lock == true :-> false;
	// }
	// // real-time performance guarantee!
	// action arraycopy(Array a, b) {
	//    duration := 20;
	//    Array temp;
	//    action read() {
	//		duration := 5;
	//		temp.data := a.data;
	//	  }
	//	  action write() {
	//		duration := 5;
	//      b.data := temp.data;
	//	  }
	//	  [all] contains ordered(lock(a),read(a),unlock(a),lock(b),write(b),unlock(b))
	// }
	// Array a,b,c;
	// a.data = "hello";
	// b.data = "world";
	// c.data = "foo";
	// [0,20] { arraycopy(a,b); arraycopy(b,c); }
	// // b/c of the duration constraint, the write to b cannot precede the read from b
	// // ergo b is read from, to temp, before the write, from temp, to b.
	// // is temp the same object in the two instances of arraycopy...or different?
	// // different is a better interpretation in context
	// // but what a colossal headache to deal with...
	// // consider that one could do
	// action foo (Type1 blah ) {
	//  Type2 a;
	//  [all] bar(a);
	//  <operations on blah>
	//  // which is 'a' of Type1 of bar()
	//  }
	// action bar (Type2 blah ) {
	//  Type1 a;
	//  [all] foo(a);
	//   <operations on blah>
	//   // which is 'a' of Type2 of foo()
	//  }
	// // So that one needs to process effects on properties of objects
	// // in such a manner that they can be read by other actions without
	// // knowing that they are reading from a local object that is
	// // instantiation dependent w.r.t. the action creating the local object
	// //
	// // One can do it by doing (#schema+1) ^ (k), where k is the maximum arity;
	// // each action is then like:
	// action fly-s1-s2-s3... (<args to s1>, <args to s2>, ... )
	// // with the +1 for the null schema, so that sometimes one simplifies to
	// action fly-null-null-... (<atomic arg 1>, <atomic arg 2>, ...)
	// // and then each of these actions then has sufficient information
	// // to find all the properties of every possible object
	// //
	// // local objects kept to local scope are much easier, but still
	// // cumbersome.  One still needs just as much storage, but
	// // there can be less schema proliferation.
	// //
	// // so for all those reasons, I'm taking 'static' as the default
	// // access for local objects/symbols.  Effectively, the referent 
	// // of the identifier is the literal text in the model -- the token.
	// // so two objects of the same name in different scopes are different
	// // objects, but two invocations of the same lexical scope with different
	// // bindings are still in the same lexical scope and so see the same
	// // referent.  In particular the arraycopy model would not have the
	// // intended effect; instead of a and b moving to b and c respectively
	// // either b and c both contain "World" or b and c both contain "Hello"
	// // [the plans that work are a little tricky to find; since temp.data
	// // is the same fluent the write effects of the read() actions are mutex]
	//
	// constants and fluents, on the other hand, do not have this problem
	// because their classes, in the sense of object types, are local to 
	// the action declaring them; in the pddl they look like
	// (foo a_x a_y a_x f_x f_y f_z) where the first set of parameters is
	// that of the action.  For an object that is kept local (not passed)
	// , as mentioned above, the situation simplifies, and context becomes
	// 'easy' to incorporate in the same manner as constants and fluents.
	// the issue is that the schema of context changes if multiple actions
	// have to access the same fluent, which isn't possible for action-local
	// fluents, but is possible for properties of action-declared, but non-local,
	// objects.
	//
	// A real machine has a memory space, and what ends up happening
	// is that the  method/function local objects end up being dynamically
	// associated with the fixed pool of constant symbols (memory locations).
	// A similar approach could be pursued in this compilation, but
	// then no pddl planner would have even a remote chance of succeeding,
	// if the symbol pool is large enough to maintain semantic consistency
	// with the anml.  An anml planner can succeed because it is running
	// on a machine with dynamic allocation, and so can dynamically allocate
	// just enough symbols for the plan under consideration, instead of
	// having to pre-allocate enough symbols to stand for simultaneously
	// executing every instantiation of fly(o,x,y).
	//
	// For any realistic model, it would be possible to bound the number
	// of concurrently accessible instances of any given type, and then employ
	// the dynamic memory approach:
	// arraycopy(Array x,y) -> (arraycopy x y - Array u v t - __Memory) 
	// Array t -> :condition (and (null t) ...)
	// Array t -> :effect (and (at start (not (null t)) (array t) (data t null) (= (length t) 0)) ... )
	// [p] t.data := a.data -> :condition (and (at start (data a u) ...) ...)
	//							:effect (... (at p (data t u)) ...)
	// and so forth; the critical part being to have an internal __Memory type
	// that is a pool of symbols standing for references to memory locations, the validity
	// and type of which is dynamically tracked.
	// so then every property would be declared as
	// (<prop> <objectarg> - ANMLObject <typed_args> )
	// and (:types __Memory - ANMLObject ...)
	// and of course any normal object type would also subclass ANMLObject
	// so that both statically and dynamically declared objects could be handled,
	// with an optimization for the statically declared case.
	public class ObjectRef implements Argument {
		public Object ref;
		public ObjectRef(Object ref) {
			super();
			this.ref = ref;
		}
		public StringBuilder append(StringBuilder buf) {
			return buf.append(ref.name);
		}
	}
	
	public class Object implements Append {
		public String name;
		public Type type;
		public Object(String name) {
			super();
			this.name = name;
			this.type = PDDL.this.Object;
		}
		public Object(String name,Type type) {
			super();
			this.name = name;
			this.type = type;
		}
		public StringBuilder append(StringBuilder buf) {
			buf.append(name).append(" - ");
			type.append(buf);
			return buf;
		}
	}

	public class Predicate {
		public String name;
		public ArrayList<Parameter> context = new ArrayList<Parameter>();
		public ArrayList<Parameter> parameters = new ArrayList<Parameter>();
		PredicateReference trivialRef=null;
		public PredicateReference trivialRef() {
			if (trivialRef != null)
				return trivialRef;
			trivialRef = new PredicateReference(this);
			// predicate references happen in the same context necessarily, so
			// PredicateReference just calls back to find the context variables
			// (PredicateReference.ref.context == this.context)
//			for (Parameter p : context) {
//				trivialRef.arguments.add(p.ref);
//			}
			for (Parameter p : parameters) {
				trivialRef.arguments.add(p.ref);
			}
			return trivialRef;
		}
		public StringBuilder append(StringBuilder buf) {
			buf.append('(').append(name);
			for (Parameter arg : context) {
				arg.append(buf.append(' '));
			}
			for (Parameter arg : parameters) {
				arg.append(buf.append(' '));
			}
			buf.append(')');
			return buf;
		}
		public Predicate(String name) {
			super();
			this.name = name;
		}
	}

	public class Function {
		public String name;
		public ArrayList<Parameter> context = new ArrayList<Parameter>();
		public ArrayList<Parameter> parameters = new ArrayList<Parameter>();
		public FunctionReference trivialRef;
		public FunctionReference trivialRef() {
			if (trivialRef != null)
				return trivialRef;
			trivialRef = new FunctionReference(this);
			for (Parameter p : parameters) {
				trivialRef.arguments.add(p.ref);
			}
			return trivialRef;
		}
		public StringBuilder append(StringBuilder buf) {
			buf.append('(').append(name);
			for (Parameter arg : context) {
				arg.append(buf.append(' '));
			}
			for (Parameter arg : parameters) {
				arg.append(buf.append(' '));
			}
			buf.append(')');
			return buf;
		}
		public Function(String name) {
			super();
			this.name = name;
		}
	}

	public class Parameter {
		public String name;
		public Type type;
		public ParameterReference ref;
		public Parameter(String name, Type type) {
			super();
			this.name = name;
			this.type = type;
			this.ref = new ParameterReference(this);
		}
		public StringBuilder append(StringBuilder buf) {
			buf.append('?').append(name).append(" - ");
			return type.append(buf);
		}
	}

	public class ParameterReference implements Argument {
		Parameter ref;
		public ParameterReference(Parameter ref) {
			super();
			this.ref = ref;
		}
		public StringBuilder append(StringBuilder buf) {
			buf.append('?').append(ref.name);
			return buf;
		}
	}

	public class PredicateReference implements BooleanExpression {
		public Predicate ref;
		public ArrayList<Argument> arguments = new ArrayList<Argument>();
		public StringBuilder append(StringBuilder buf) {
			buf.append('(').append(ref.name);
			for (Parameter p : ref.context) {
				p.ref.append(buf.append(' '));
			}
			for (Argument arg : arguments) {
				arg.append(buf.append(' '));
			}
			buf.append(')');
			return buf;
		}
		public PredicateReference(Predicate ref) {
			super();
			this.ref = ref;
		}
		public boolean isTimed() {
			return false;
		}
	}

	public class FunctionReference implements FloatExpression {
		public Function ref;
		public ArrayList<Argument> arguments = new ArrayList<Argument>();
		public FunctionReference(Function ref) {
			super();
			this.ref = ref;
		}
		public StringBuilder append(StringBuilder buf) {
			buf.append('(').append(ref.name);
			for (Parameter p : ref.context) {
				p.ref.append(buf.append(' '));
			}
			for (Argument arg : arguments) {
				arg.append(buf.append(' '));
			}
			buf.append(')');
			return buf;
		}
		public boolean isTimed() {
			return false;
		}
	}

	public static PDDL.Time getShape(Interval i) {
		//gov.nasa.anml.lifted.Constant<SimpleFloat> s,d,e;
		gov.nasa.anml.lifted.Constant<SimpleInteger> b,k;
		
		b = i.getBra();
//		s = i.getStart();
//		d = i.getDuration();
//		e = i.getEnd();
		k = i.getKet();
		
		// null might be a better return; or a new code
		// for indeterminate shape
		if (b.value == null || k.value == null)
			return PDDL.Time.Timeless;
		
		switch(b.value.v) {
		case gov.nasa.anml.lifted.Time.Before:
		case gov.nasa.anml.lifted.Time.At:
			switch(k.value.v) {
			case gov.nasa.anml.lifted.Time.Before:
					return PDDL.Time.StartHalf;
			case gov.nasa.anml.lifted.Time.At:
			case gov.nasa.anml.lifted.Time.After:
				return PDDL.Time.All;
			}
		case gov.nasa.anml.lifted.Time.After:
			switch(k.value.v) {
			case gov.nasa.anml.lifted.Time.Before:
					return PDDL.Time.Interim;
			case gov.nasa.anml.lifted.Time.At:
			case gov.nasa.anml.lifted.Time.After:
				return PDDL.Time.EndHalf;
			}
		}
		
		return PDDL.Time.Timeless;
	}
	
	// works only if t is in fact some piece of s, so that its start/end/duration/bra/ket refer to
	// the parent's variables _by reference_.  This is what will happen by default in the parser.
	public static PDDL.Time getPart(Interval s, Interval t) {
		gov.nasa.anml.lifted.Expression<SimpleFloat,?> s1,e1,s2,e2;
		s1 = s.getStart();
		s2 = t.getStart();
		e1 = s.getEnd();
		e2 = t.getEnd();
		if (s1 == s2) {
			if (e1 == e2) {
				SimpleInteger b = t.getBra().value(null);
				SimpleInteger k = t.getKet().value(null);
				if (b == null || k == null)
					return null;
				if (b.v > 0) {
					if (k.v < 0)
						return PDDL.Time.Interim;
					else
						return PDDL.Time.EndHalf;
				} else {
					if (k.v < 0)
						return PDDL.Time.StartHalf;
					else
						return PDDL.Time.All;
				}
			} else if (s1 == e2) {
				return PDDL.Time.Start;
			}
			return null;
		} else if (e1 == s2 && s2 == e2) {
			return PDDL.Time.End;
		}

		//System.err.println("OOOPS");
		return PDDL.Time.Timeless;
	}

	public class Action {
		public String name = "";
		public ArrayList<Parameter> context = new ArrayList<Parameter>();
		public ArrayList<Parameter> parameters = new ArrayList<Parameter>();

		public FloatExpression duration = Zero;

		public CompoundBooleanExpression condition = new CompoundBooleanExpression(Op.and);
		public CompoundEffect effect = new CompoundEffect(Op.and);
	
		public Predicate executing;

		// can invert to executable if negative preconditions are frowned upon, i.e., sapa
		// in that case, the (now negative) interim condition can be omitted b/c we would only
		// do this in a pure STRIPS context, so that testing for the negative is guaranteed redundant.
		// Either that, or do the negative split ourself (track an executable and an executing).
		public Predicate makeExecuting() {
			if (executing == null) {
				executing = new Predicate(this.name + "_executing");
				executing.context.addAll(context);
				executing.parameters.addAll(parameters);
				// consider being smarter about these.
				PredicateReference trivialRef = executing.trivialRef();
				//condition.arguments.add(new TimedBooleanExpression(Time.Start,new UnaryBooleanExpression(Op.not,trivialRef)));
				condition.arguments.add(new TimedBooleanExpression(Time.Interim,trivialRef));
				effect.arguments.add(wrap(Time.Start,new AtomicBooleanEffect(trivialRef,true)));
				effect.arguments.add(wrap(Time.End,new AtomicBooleanEffect(trivialRef,false)));
				predicates.add(executing);
			}
			return executing;
		}

		public Action() {
			super();
		}
		
		public Action(String name) {
			super();
			this.name = name;
			// makeExecutingPredicate();
			// only make the executing predicate for real anml actions, not helper actions
		}

		public StringBuilder append(StringBuilder buf) {
			buf.append("(:durative-action ").append(name);
			if (parameters.isEmpty()) {
				buf.append("\n:parameters ()\n:duration (= ?duration ");
			} else {
				buf.append("\n:parameters (");
				for(Parameter p : context) {
					p.append(buf).append(' ');
				}
				for(Parameter p : parameters) {
					p.append(buf).append(' ');
				}
				buf.setCharAt(buf.length()-1,')');
				buf.append("\n:duration (= ?duration ");
			}
			duration.append(buf);
			buf.append(")\n:condition ");
			condition.append(buf);
			buf.append("\n:effect ");
			effect.append(buf);
			buf.append("\n)\n");
			return buf;
		}
	}
 
	// the duration field can be empty, and yet durations can still be constrained
	// as normal conditions.  Technically.
	public class ComplexAction extends Action {
		public BooleanExpression durationConstraint = new CompoundBooleanExpression(Op.and);
		{
			duration = null;
		}

		public ComplexAction() {
			super();
		}
		public ComplexAction(String name) {
			super(name);
		}

		public StringBuilder append(StringBuilder buf) {
			buf.append("(:durative-action ").append(name);
			if (parameters.isEmpty()) {
				buf.append("\n:parameters ()\n:duration ");
			} else {
				buf.append("\n:parameters (");
				for(Parameter p : context) {
					p.append(buf).append(' ');
				}
				for(Parameter p : parameters) {
					p.append(buf).append(' ');
				}
				buf.setCharAt(buf.length()-1,')');
				buf.append("\n:duration ");
			}
			durationConstraint.append(buf);
			buf.append("\n:condition ");
			condition.append(buf);
			buf.append("\n:effect ");
			effect.append(buf);
			buf.append("\n)\n");
			return buf;
		}
	}

	public enum Op {
		plus("+"),
		minus("-"),
		times("*"),
		divided_by("/"),
		increase("increase"),
		decrease("decrease"),
		assign("="), // should be assign("assign"), but that makes handling initial state ugly
		equals("="),
		lte("<="),
		gte(">="),
		lt("<"),
		gt(">"),
		and("and"),
		or("or"),
		not("not"),
		implies("imply"),
		when("when"),
		exists("exists"),
		forall("forall"),
		;

		public String name;
		private Op(String n) {
			name = n;
		}

		public String toString () {
			return name;
		}

		public StringBuilder append(StringBuilder buf) {
			return buf.append(name);
		}
	}

	public class ConditionalEffect implements Effect {
		public BooleanExpression guard;
		public Effect eff;
		public ConditionalEffect(BooleanExpression g, Effect e) {
			guard = g;
			eff = e;
		}
		public StringBuilder append(StringBuilder buf) { 
			indent(buf);
			buf.append("(when ");
			guard.append(buf).append(' ');
			eff.append(buf).append(')');
			dedent(buf);
			return buf;
		}
	}

	public class AtomicBooleanEffect implements BooleanEffect {
		public PredicateReference ref;
		public boolean v;
		public AtomicBooleanEffect(PredicateReference ref, boolean v) {
			this.ref = ref;
			this.v = v;
		}
		public StringBuilder append(StringBuilder buf) {
			if (v)
				return ref.append(buf);
			buf.append("(not ");
			return ref.append(buf).append(')');
		}
	}

	public class AtomicFloatEffect implements FloatEffect {
		public Op o;
		public FunctionReference ref;
		public FloatExpression e;
		public AtomicFloatEffect(Op o, FunctionReference ref, FloatExpression e) {
			this.o = o;
			this.ref = ref;
			this.e = e;
		}
		public StringBuilder append(StringBuilder buf) {
			buf.append('(').append(o.name).append(' ');
			ref.append(buf).append(' ');
			e.append(buf).append(')');
			return buf;
		}
	}

	public class Exists implements BooleanExpression {
		public ArrayList<Parameter> parameters = new ArrayList<Parameter>();
		public BooleanExpression c;
		public StringBuilder append(StringBuilder buf) { 
			indent(buf);
			buf.append('(').append(Op.exists.name);
			parameters.get(0).append(buf.append(" ("));
			for (int i=1; i < parameters.size(); ++i) {
				parameters.get(i).append(buf.append(' '));
			}
			buf.append(')');
			c.append(buf.append(' '));
			buf.append(')');
			dedent(buf);
			return buf;
		}
		public Exists(ArrayList<Parameter> parameters, BooleanExpression c) {
			super();
			this.c = c;
			this.parameters = parameters;
		}
		public boolean isTimed() {
			return c.isTimed();
		}
	}
	
	public class ForAll implements BooleanExpression {
		public ArrayList<Parameter> parameters = new ArrayList<Parameter>();
		public BooleanExpression c;
		public StringBuilder append(StringBuilder buf) { 
			indent(buf);
			buf.append('(').append(Op.forall.name);
			parameters.get(0).append(buf.append('('));
			for (int i=1; i < parameters.size(); ++i) {
				parameters.get(i).append(buf.append(' '));
			}
			buf.append(')');
			c.append(buf.append(' '));
			buf.append(')');
			dedent(buf);
			return buf;
		}
		public ForAll(ArrayList<Parameter> parameters, BooleanExpression c) {
			super();
			this.c = c;
			this.parameters = parameters;
		}
		public boolean isTimed() {
			return c.isTimed();
		}
	}

	public class Binary<T extends Append> {
		public Op o;
		public T l;
		public T r;
		public Binary(Op o, T l, T r) {
			this.o = o;
			this.l = l;
			this.r = r;
		}
		public StringBuilder append(StringBuilder buf) { 
			//indent(buf);
			buf.append('(').append(o.name).append(' ');
			l.append(buf).append(' ');
			r.append(buf).append(')');
			//dedent(buf);
			return buf;
		}
	}
	
	public class Unary<T extends Append> {
		public Op o;
		public T l;
		public Unary(Op o, T l) {
			this.o = o;
			this.l = l;
		}
		public StringBuilder append(StringBuilder buf) {
			buf.append('(').append(o.name).append(' ');
			l.append(buf).append(')');
			return buf;
		}
	}
	public class UnaryExpression extends Unary<Expression> implements Expression {
		public UnaryExpression(Op o, Expression e) { super(o,e); }
	}
	// i.e., the not function.  Albeit, set high, set low, and pass through are also functions --
	// just not overly useful ones.
	public class UnaryBooleanExpression extends Unary<BooleanExpression> implements BooleanExpression {
		public UnaryBooleanExpression(Op o, BooleanExpression e) { super(o,e); }
		public boolean isTimed() {
			return l.isTimed();
		}
	}
	public class UnaryFloatExpression extends Unary<FloatExpression> implements FloatExpression {
		public UnaryFloatExpression(Op o, FloatExpression e) { super(o,e); }
		public boolean isTimed() {
			return l.isTimed();
		}
	}
	public class UnaryEffect extends Unary<Effect> implements Effect {
		public UnaryEffect(Op o, Effect e) { super(o,e); }
	}
	public class BinaryEffect extends Binary<Effect> implements Effect{
		public BinaryEffect(Op o, Effect l, Effect r) {super(o,l,r);}
	}
	public class BinaryBooleanEffect extends Binary<BooleanEffect> implements BooleanEffect {
		public BinaryBooleanEffect(Op o, BooleanEffect l, BooleanEffect r) {super(o,l,r);}
	}

	
	public class BinaryExpression extends Binary<Expression> implements Expression {
		public BinaryExpression(Op o, Expression l, Expression r) {
			super(o, l, r);
		}
	}
	
	public class BinaryBooleanExpression extends Binary<BooleanExpression> implements BooleanExpression {
		public BinaryBooleanExpression(Op o, BooleanExpression l, BooleanExpression r) {
			super(o, l, r);
		}
		public boolean isTimed() {
			return l.isTimed() && r.isTimed();
		}
		public StringBuilder append(StringBuilder buf) { 
			indent(buf);
			buf.append('(').append(o.name).append(' ');
			l.append(buf).append(' ');
			r.append(buf).append(')');
			dedent(buf);
			return buf;
		}
	}
	public class BinaryFloatExpression extends Binary<FloatExpression> implements FloatExpression {
		public BinaryFloatExpression(Op o, FloatExpression l, FloatExpression r) {
			super(o, l, r);
		}
		public boolean isTimed() {
			return l.isTimed() && r.isTimed();
		}
	}
	
	public class RelOp extends Binary<FloatExpression> implements BooleanExpression {

		public RelOp(Op o, FloatExpression l, FloatExpression r) {
			super(o, l, r);
		}
		public boolean isTimed() {
			return l.isTimed() && r.isTimed();
		}
		
	}
	
	public class FloatLiteral implements FloatExpression, Timed<FloatExpression> {
		public float v;
		public FloatLiteral(float v) {
			this.v = v;
		}
		public StringBuilder append(StringBuilder buf) {
			return buf.append(v);
		}		
		public boolean isTimed() {
			return true;
		}
	}

	public class CompoundExpression extends Compound<Expression> implements Expression {
		public CompoundExpression(Op o) { super(o); }

		public CompoundExpression(Op o, Expression a, Expression b) {
			super(o, a, b);
		}

		public CompoundExpression(Op o, Expression a) {
			super(o, a);
		}
		
	}
	
	public class CompoundBooleanExpression extends Compound<BooleanExpression> implements BooleanExpression {
		public CompoundBooleanExpression(Op o) { super(o); }

		public CompoundBooleanExpression(Op o, ArrayList<BooleanExpression> args) {
			super(o, args);
		}
		
		public CompoundBooleanExpression(Op o, BooleanExpression a, BooleanExpression b) {
			super(o, a, b);
		}

		public CompoundBooleanExpression(Op o, BooleanExpression a) {
			super(o, a);
		}
		
		public boolean isTimed() {
			for(int i=0; i<arguments.size();++i) {
				if (!arguments.get(i).isTimed())
					return false;
			}
			return true;
		}
		
	}

	public class CompoundEffect extends Compound<Effect> implements Effect {
		public CompoundEffect(Op o) { super(o); }

		public CompoundEffect(Op o, ArrayList<Effect> args) { 
			super(o,args); 
		}

		public CompoundEffect(Op o, Effect a, Effect b) {
			super(o, a, b);
		}

		public CompoundEffect(Op o, Effect a) {
			super(o, a);
		}
	}

	public enum Time {
		Start("at start"),  // 'before' for conditions and expressions, 'at' for effects
		Interim("over all"), // (all)
		End("at end"), // 'before' for conditions and expressions, 'at' for effects

		// below are all the super-intervals of the atomically accessible intervals (above)
		// only useful during translation, maybe not even then
		All("[all]"),
		StartHalf("[all)"),
		EndHalf("(all]"),
		
		Timeless(""),
		
		;

		public String name;
		private Time(String s) {
			name = s;
		}
	}

	public class TimedBooleanExpression extends TimedImp<BooleanExpression> implements BooleanExpression {
		public TimedBooleanExpression(Time time, BooleanExpression b) {	super(time,b); }
		public boolean isTimed() {
			return true;
		}
	}
	
	public class TimedFloatExpression extends TimedImp<FloatExpression> implements FloatExpression {
		public TimedFloatExpression(Time time, FloatExpression b) {	super(time,b); }
		public boolean isTimed() {
			return true;
		}
	}

	
	public abstract class TimedImp<T extends Append> implements Timed<T> {

		public Time time;
		public T e;
		public TimedImp(Time time, T e) {
			if (e == null)
				System.err.println("Oopsies: null expression in a timed expression");
			this.time = time;
			this.e = e;
		}
		public StringBuilder append(StringBuilder buf) {
			indent(buf);
			buf.append('(').append(time.name).append(' ');
			e.append(buf).append(')');
			dedent(buf);
			return buf;
		}
	}
	
	public class TimedEffect<T extends Effect> extends TimedImp<T> implements Effect {
		public TimedEffect(Time time, T e) {super(time, e);}
	}
	
	public class TimedBooleanEffect extends TimedEffect<BooleanEffect> implements BooleanEffect {
		public TimedBooleanEffect(Time time, BooleanEffect e) {super(time,e);}
	}
	
	public class TimedFloatEffect extends TimedEffect<FloatEffect> implements FloatEffect {
		public TimedFloatEffect(Time time, FloatEffect e) {super(time,e);}
	}



	public final Predicate Alive = new Predicate("alive");
	public final PredicateReference AliveRef = new PredicateReference(Alive);
	public final Predicate True = new Predicate("true");
	public final PredicateReference TrueRef = new PredicateReference(True);
	public final UnaryBooleanExpression FalseRef = new UnaryBooleanExpression(Op.not,TrueRef);
	public final TimedBooleanExpression TrueCondition = new TimedBooleanExpression(Time.Interim,TrueRef);
	public final TimedBooleanExpression FalseCondition = new TimedBooleanExpression(Time.Interim,FalseRef);
	public final FloatLiteral One = new FloatLiteral(1.0f);
	public final FloatLiteral Zero = new FloatLiteral(0.0f);
	public final FloatExpression FloatUndefined = new BinaryFloatExpression(Op.divided_by,One,Zero);
	public final Type Object = new Type("object");
	private final Object Null = new Object("null");
	public final ObjectRef NullRef = new ObjectRef(Null);
	public final Function DurationParameter = new Function("?duration");
	public final FunctionReference DurationRef = new FunctionReference(DurationParameter);
	
	

	public class Problem {
		public String name;
		public ArrayList<ObjectRef> objects = new ArrayList<ObjectRef>();
		public State init = new State();
		public Goal goal = new Goal();
		public Problem(String name) {
			super();
			this.name = name;
		}
		public Problem() {
		}
		public StringBuilder append(StringBuilder buf) {
			buf.append("(define (problem ").append(name)
			.append(")\n(:domain ").append(PDDL.this.name).append(")\n(:objects");
			for (ObjectRef o : objects) {
				o.append(buf.append(' '));
			}
			buf.append(")\n");
			init.append(buf);
			goal.append(buf);
			buf.append("\n\n)\n");
			return buf;
		}
	}

	public class State {
		public ArrayList<Effect> effects = new ArrayList<Effect>();
		public StringBuilder append(StringBuilder buf) {
			buf.append("(:init (true)");
			for (Effect e : effects) {
				e.append(buf.append("\n\t"));
			}
			buf.append("\n)\n");
			return buf;
		}
	}

	public class Goal {
		public ArrayList<BooleanExpression> booleanExpressions = new ArrayList<BooleanExpression>();
		public StringBuilder append(StringBuilder buf) {
			buf.append("(:goal (and");
			for (BooleanExpression c : booleanExpressions) {
				c.append(buf.append("\n\t"));
			}
			buf.append("\n\t)\n)\n");
			return buf;
		}
	}

	static StringBuilder newlineAndIndent = new StringBuilder("\n\t");
	protected void indent(StringBuilder buf) {
		buf.append(newlineAndIndent);
		newlineAndIndent.append('\t');
	}
	protected void dedent(StringBuilder buf) {
		newlineAndIndent.setLength(newlineAndIndent.length()-1);
	}

}
